COMMENT ⊗   VALID 00010 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.device xgp
C00005 00003	.once center
C00017 00004	.next page
C00029 00005	.NEXT PAGE FILL ADJUST INDENT 0,0,0 PREFACE 1
C00037 00006	.SKIP 2
C00041 00007	.once center
C00043 00008	.once center
C00045 00009	.once center
C00049 00010	∂24-Apr-78  1202	Levin at SUMEX-AIM 	brief biographical info on referees for manna
C00055 ENDMK
C⊗;
.device xgp
.!XGPCOMMANDS ← "/TMAR=200/PMAR=1900/BMAR=100"
.turn on "%,π,α,#,&,→"
.turn on "∩" for "↑"
.font 1 "nonm"
.font 2 "basi30"
.font 3 "nonmb"
.<<FONT 4 "SUB"
.FONT 5 "SUP">>
.font 4 "mathx[pub,pat]"
.FONT 6 "FORN25"
.FONT 7 "FIX25"
.FONT 8 "MISC25"
.FONT 9 "PLUNK"
.FONT A "GRFX25"
.FONT B "BASB30"
.FONT C "CLAR30"
.FONT D "MATH50"
.FONT E "FIX20"
.FONT F "CLAR40"
.SINGLESCRIPT
.SPACING 10*5 MILLS;
.PAGE FRAME 45 HIGH 78 WIDE
.TITLE AREA HEADING LINES 1 TO 2
.AREA TEXT LINES 3 TO 43
.TITLE AREA FOOTING LINE 45
.SELECT 1
.EVERY FOOTING (,{PAGE})
.COUNT PAGE from 1;
.AT "[" TXT "]"; ⊂("%2TXT%*")⊃;
.at "⊗⊗" txt "⊗"; ⊂("%3txt%*")⊃;
.at "≤" ⊂"%7α≤%*"⊃
.at "≥" ⊂"%7α≥%*"⊃
.at "↓" txt "↑" ⊂"%4txt%*"⊃
.at "↑" txt "↓" ⊂"%5txt%*"⊃
.at "!∞" ⊂"%7α∞%*"⊃
.AT "!$" ⊂"%Dα$%*"⊃
.at "!cd" ⊂"%7π.%*"⊃
.at "!'" ⊂"%8α'%*"⊃
.at "-" ⊂"%6α-%*"⊃
.at "¬" ⊂"%6α¬%*"⊃
.at "!ε" ⊂"%9αB%*"⊃
.at "!≤" ⊂"%8α≤%*"⊃
.at "<=>" ⊂"%7α<α=α>%*"⊃
.at "=>" ⊂"%7α=α>%*"⊃
.at "≠" ⊂"%7α≠%*"⊃
.at "|" ⊂"%6α|%*"⊃
.AT "∞" ⊂"%9α[%*"⊃
.at "∂" ⊂"%9α]%*"⊃
.AT "@" ⊂"%Aαα%*"⊃
.at "~" ⊂"%5α*%*"⊃
.at "!D" ⊂"%4α⊗%*"⊃
.macro bi; ⊂
.indent 8,12,8;
.turn on "\"; tabs 13;
. ⊃
.macro bf; ⊂
.crbreak; nojust;
.preface 0; turn on "\";
.tabs 10,19,23;
. ⊃
.macro bd; ⊂
.group
.crbreak; nojust;
.preface 0; turn on "\";
. ⊃
.macro bib (NUM,NAM) ; ⊂
.nofill; preface 1;
.indent 0
.turn on "\";
.TABS 7
NUM.\NAM
.fill; preface 0; spacing 10*5 mills;
.indent 6,6,6
. ⊃
.PLACE TEXT
.next page
.once center
%3II. BIOGRAPHICAL INFORMATION %*
.skip
.begin nofill
Name:  ⊗⊗Zohar Manna⊗
Born:  January 17, 1939 (Haifa, Israel)
Dual citizenship:  Israel and United States
.end
.skip
!D  %3Education and Work:%*
.skip
.begin bd; apart;
.tabs 12,38,48
1958-1962\Undergraduate Student
\Mathematics Department
\Technion, Haifa, Israel
\B.Sc. (1962)
.skip
1962-1964\Israel Defense Forces
\First Lieutenant
\Scientific Programming
.skip
1964-1965\Graduate Student
\Mathematics Department
\Technion, Haifa, Israel
\M.Sc. (1965)
.skip
1965-1968\Graduate Student
\Computer Science Department
\Carnegie-Mellon University
\Pittsburgh, Pennsylvania
\Ph.D. (1968)
.skip
1968-1971\Assistant Professor
\Computer Science Department
\Stanford University
\Stanford, California
.skip
1971-1972\Visiting Associate Professor
\Computer Science Dept.
\Stanford University
\Stanford, California
.next page
1972-1976\Associate Professor
\Applied Mathematics Dept.
\Weizmann Institute
\Rehovot, Israel
.skip
1976-\Professor\1975-####\Research Associate
\Applied Mathematics Dept.\\Artificial Intelligence Lab
\Weizmann Institute\\Stanford University
\Rehovot, Israel\\Stanford, California
.end
.skip 2
!D  %3Scholarships and academic honors%*

.begin nofill
Undergraduate study - cum laude
HTI Graduate Scholarship
Landau Science Award (1976)
.end
.skip 
!D  %3Memberships%1

.begin nofill
Association for Computer Machinery
The Insitute of Electrical and Electronics Engineers
European Association for Theoretical Computer Science
.end
.skip
!D  %3Associate Editor of:%*

.begin nofill
Computer Languages Journal
Acta Informatica
Theoretical Computer Science Journal
.end
.skip
!D  %3Research Interests:%*

.begin nofill
Mathematical Theory of Computation
Program Verification and Synthesis
Methodology of Programming
Programming Languages
.end
.skip 
!D  %3Special Committees%*

Council member of the European Association for Theoretical Computer Science

Member of the Theory of Computing Panel of the NSF Computer Science and
Engineering Research Study.
.skip
!D  %3Public Service%*

.begin nofill
	1. Member of the Theory of Computing Panel of the NSF Computer
Science and Engineering Research Study (COSERS).
%*
	2. Council member of the European Association for Theoretical
Computer Science.

	3. Member of IFIP 2.2 working group: Formal description of
programming concepts.

	4. Member of program committee of about 12 conferences.

	5. Associate editor of three journals: Computer Language Journal,
Acta Informatica, and Theoretical Computer Science Journal.
.end
.skip
!D  %3Current Grants/Contracts:%*

At Stanford University:
National Science Foundation (Grant MCS 76-83655)
Office of Naval Research (Contract NOOO14-76-C-0687)
Advanced Research Projects Agency (Part of Contract MDA 903-76-C-0206)

At the Weizmann Institute:
United States Air Force Office of Scientific Research (Grant AFOSR-76-2909)
United States-Israel Binational Science Foundation (Grant 574)
.skip 
!D  %3Major invited papers and addresses%*

1.##%2Automatic programming%1, Third International Joint Conference on Artificial
Intelligence, Stanford, CA (August 1973).

2.##%2Towards automatic debugging of programs%1, First International Conference
on Reliable Software, Los Angeles, CA (April 1975).

3.##%2On automating structured programming%1, International Symposium on Proving
and Improving Programs, Arc-et-Senans, France (July 1975).

4.##%2The recursive way of thinking%1, Carnegie-Mellon 
University Computer Science Department 10∩[th] Anniversary
Symposium, Pittsburgh, PA (October 1975).

5.##%2Intermittent assertions in proving program correctness%1, Second International
Conference on Software Engineering, San Francisco, CA (October 1976).

6.##%2New trends in program verification%1, Computer Science Conference, Atlanta,
GA (January 1977).

7.##%2The fixedpoint theory of recursive programs%1, American Mathematical
Society Meeting, San Luis Obispo, CA (November 1977).

8.##%2Program verification without magic%1, Third International Conference on Software
Engineering, Atlanta, GA (May 1978).

9.##%2The DEDALUS system%1, National Computer Conference, Anaheim, CA (June 1978).
.next page
.once center
%3III. BIBLIOGRAPHICAL INFORMATION%*

.tabs 9
.bib(1,|Z. Manna α[April 1969α]|)
[Properties of programs and the first]-[order predicate calculus], ⊗⊗Journal
of the ACM⊗, Vol. 16, No. 2, pp. 244-255.

.bib(2,|Z. Manna α[May 1969α]|)
[The correctness of programs], ⊗⊗Journal of Computer and System Sciences⊗,
Vol. 3, No. 2, pp. 119-127.

.bib(3,|Z. Manna α[May 1970α]|)
[Termination of algorithms represented as interpreted graphs], AFIPS Conference
Proceedings, Vol. 36, pp. 83-90.

.bib(4,|Z. Manna α[May 1970α]|)
[Second]-[order mathematical theory of computation], Proceedings of the ACM
Symposium on Theory of Computing, pp. 158-168.

.bib(5,|Z. Manna and A. Pnueli α[July 1970α]|)
[Formalization of properties of functional programs], ⊗⊗Journal of the ACM⊗,
Vol. 17, No. 3, pp. 555-569.

.bib(6,|Z. Manna α[1970α]|)
[The correctness of non]-[deterministic programs], ⊗⊗Artificial Intelligence⊗,
Vol. 1, No. 1, pp. 1-26.

.bib(7,|Z. Manna and J. McCarthy α[1970α]|)
[Properties of programs and partial function logic], ⊗⊗Machine Intelligence 5⊗
(Eds. Meltzer and Michie), Edinburgh University Press, pp. 79-98.

.bib(8,|Z. Manna and R. Waldinger α[March 1971α]|)
[Toward automatic program synthesis], ⊗⊗Communication of the ACM⊗, Vol. 14,
No. 3, pp. 151-165.

.bib(9,|Z. Manna α[June 1971α]|)
[Mathematical theory of partial correctness], ⊗⊗Journal of Computer and System
Sciences⊗, Vol. 5, No. 3, pp. 239-253.

.bib(10,|E. Ashcroft and Z. Manna α[1971α]|)
[Formalization of properties of parallel programs], ⊗⊗Machine Intelligence 6⊗
(Eds. Meltzer and Michie), Edinburgh University Press, pp. 17-41.

.bib(11,|J. M. Cadiou and Z. Manna α[January 1972α]|)
[Recursive definitions of partial functions and their computations], Proceedings
of the ACM Conference on Proving Assertions about Programs, Las Cruces, 
New Mexico, pp. 58-65.

.bib(12,|A. Chandra and Z. Manna α[May 1972α]|)
[Program schemas with equality], Proceedings of the ACM Symposium on Theory of
Computing, pp. 52-64.

.bib(13,|Z. Manna α[May 1972α]|)
[Computation of recursive programs] - [theory vs practice], AFIPS Conference
Proceedings, Vol. 40, pp. 219-223.

.bib(14,|Z. Manna and J. Vuillemin α[July 1972α]|)
[Fixpoint approach to the theory of computation], ⊗⊗Communications of the ACM⊗,
Vol. 15, No. 7, pp. 528-536. Invited paper - ⊗⊗special 25th anniversary issue⊗.

.bib(15,|E. Ashcroft, Z. Manna and A. Pnueli α[July 1973α]|)
[Decidable properties of monadic functional schemas], ⊗⊗Journal of the ACM⊗,
Vol. 20, No. 3, pp. 489-499.

.bib(16,|Z. Manna, S. Ness and J. Vuillemin α[August 1973α]|)
[Inductive methods for proving properties of programs], ⊗⊗Communications of
the ACM⊗, Vol. 16, No. 8, pp. 491-502. ACM Programming System and Languages -
⊗⊗Best paper Award for 1974⊗.
          
.bib(17,|S. Katz and Z. Manna α[August 1973α]|)
[A heuristic approach to program verification], Proceedings of the Third
International Joint Conference on Artificial Intelligence, Stanford, California,
pp. 500-512.

.bib(18,|Z. Manna and A. Pnueli α[1974α]|)
[Axiomatic approach to total correctness], ⊗⊗Acta Informatica⊗, Vol. 3, 
pp. 243-263.

.bib(19,|S. Katz and Z. Manna α[April 1975α]|)
[Towards automatic debugging of programs], Proceedings of the International
Conference on Reliable Software, Los Angeles, California. ⊗⊗Invited paper⊗.

.bib(20,|E. Ashcroft and Z. Manna α[June 1975α]|)
[Translating program schemas to while]-[schemas], ⊗⊗SIAM Journal on Computing⊗,
Vol. 4, No. 2, pp. 125-146.

.bib(21,|N. Dershowitz and Z. Manna α[July 1975α]|)
[On automating structured programming], Proceedings of the International 
Symposium on Proving and Improving Programs, Arc-et-Senans, France, pp. 167-193.
%3Invited paper.%1

.bib(22,|A. Chandra and Z. Manna α[September 1975α]|)
[On the power of programming features], ⊗⊗Computer Languages⊗, Vol. 1, No. 3,
pp. 219-232.

.bib(23,|Z. Manna and R. Waldinger α[1975α]|)
[Knowledge and reasoning in program synthesis], ⊗⊗Artificial Intelligence⊗,
Vol. 6, No. 2, pp. 175-208.

.bib(24,|S. Katz and Z. Manna α[1975α]|)
[A closer look at termination], ⊗⊗Acta Informatica⊗, Vol. 5, pp. 333-352.
Also in [Current Trends in Programming Methodology], [Vol. II]:  [Program Verification]
(R. Yeh, editor), Prentice-Hall Inc., 1977.

.bib(25,|S. Katz and Z. Manna α[April 1976α]|)
[Logical analysis of programs], ⊗⊗Communications of the ACM⊗, Vol. 19,
No. 4, pp.188-206.

.bib(26,|Z. Manna and A. Shamir α[Spetember 1976α]|)
[The theoretical aspects of the optimal fixedpoint], ⊗⊗SIAM Journal of
Computing⊗, Vol. 5, No. 3, pp. 414-426.
          
.bib(27,|Z. Manna and R. Waldinger α[August 1977α]|)
[The automatic synthesis of recursive programs],
Proceedings of the
Fifth International Joint Conference on Artificial Intelligence, Cambridge, MA,
pp. 405-411.

.bib(28,|N. Dershowitz and Z. Manna α[November 1977α]|)
[The evolution of programs:  A system for automatic program modification],
IEEE Transactions on Software Engineering, Vol. 3, No. 5, pp. 377-385.

.bib(29,|Z. Manna and A. Shamir α[November 1977α]|)
[The optimal]-[fixedpoint approach to recursive programs], ⊗⊗Communications 
of the ACM⊗, Vol. 20, No. 11, pp. 824-831.  Also in [Perspective on Computer Science]
(A. K. Jones, editor), ⊗⊗Academic Press⊗, 1977, pp. 103-124.

.bib(30,|Z. Manna and R. Waldinger α[February 1978α]|)
[Is ""sometime"" sometimes better than always?  Intermittent assertions in proving
program correctness], ⊗⊗Communications of the ACM⊗, Vol. 21, No. 2, pp. 159-172.

.bib(31,|Z. Manna and A. Shamir α[March 1978α]|)
[The convergence of functions to fixedpoints of recursive definitions], ⊗⊗Theoretical
Computer Science Journal⊗, Vol. 4, No. 1.

.bib(32,|Z. Manna and R. Waldinger α[May 1978α]|)
[The logic of computer programming], ⊗⊗IEEE Transactions on Software Engineering⊗,
Vol. SE-4, No. 1.

.bib(33,|N. Dershowitz and Z. Manna α[May 1978α]|)
[Inference rules for program annotation], Proceedings of the Third International
Conference on Software Engineering, Atlanta, GA.

.bib(34,|Z. Manna and R. Waldinger α[June 1978α]|)
[The DEDALUS system], Proceedings of the 1978 National Computer Conference. 
⊗⊗Invited paper⊗.

.bib(35,|Z. Manna and R. Waldinger|)
[Synthesis]:  [dreams] => [programs], ⊗⊗Communications of the ACM⊗ (to appear).


.skip 2
.begin indent 0;
!D  %3Books:%*
.end

.tabs 9
.bib(1,|Z. Manna α[1973α],|)
[Program schemas], Chapter 3 in ⊗⊗Currents in the theory of computing⊗
(A. Aho, editor), Prentice-Hall, Englewood Cliffs, NJ.

.bib(2,|Z. Manna α[1974α],|)
⊗⊗Mathematical theory of computation⊗, McGraw-Hill, New York, NY.
α[Japanese translation (1976), International student edition (1977), Italian
translation (1978), Russian translation (to appear)α].

.bib(3,|Z. Manna and R. Waldinger (editors)α[1977α],|)
⊗⊗Studies in automatic programming logic⊗, American-Elsevier,
New York, NY.

.bib(4,|Z. Manna and R. Waldinger,|)
A textbook on program verification and synthesis, program transformation and
optimization, and related topics.  In preparation.

.NEXT PAGE; FILL ADJUST INDENT 0,0,0; PREFACE 1
.BEGIN CENTER; preface 0;
%3COMMENTS ON MANNA'S MOST IMPORTANT PUBLICATIONS
by John McCarthy, Professor of Computer Science%*
.END

1. %2Mathematical Theory of Computation%1, McGraw-Hill, New York 1974.

	This book, which has already been translated into Japanese,
Italian and Russian and reprinted as a paperback, is the first textbook
in mathematical theory of computation.
Its appearance is a major step towards replacing experimental debugging
of computer programs by proofs that they meet their specifications.

	At present, computer programs are debugged.  That is, after
a program is written it is tried on test cases until its author is
satisfied and turns it over to users.  If the program is at all
complex, the users usually find further mistakes.  Mistakes turn
up in big systems for years.  The mistakes often cause economic loss
and the cost of fixing them often exceeds the cost of the original
program many times over.

	The major applied goal of mathematical theory of computation
is to replace debugging by mathematically proving that the program
meets its specifications.  Such a proof must then be checked either
by a person or by a proof-checking computer program.  Once this has
been done, the chance of error is reduced to that of an incongruity
between the formal specifications and what the users have in mind
or to an error in the proof-checking program or on the part of the
human checking the proof.  Computer scientists believe that
formal proving will bring about a major reduction in the cost
of getting good programs.

	Manna's text is the first big step in making these techniques
accessible to students of computer science at an early stage.  Writing
the first textbook in a new field is a major creative endeavor, and
Manna's book is not a mere summary of research papers.  The high regard
the computer science world has for the book is shown by the number
of translations into foreign languages.

	It is a first class scholarly work in that it reworks and presents not
only the approaches to program proving that Manna himself has worked on,
but also the other major approaches and necessary background material
from mathematical logic, recursive function theory and the theory of
automata.

2. "Properties of programs and the first-order predicate calculus",
%2Journal of the Association for Computing Machinery%1, Vol. 16,
No. 2, pp. 244-255. April 1969.

	This paper, based on Manna's Ph.D. thesis, shows how to
write sentences of the predicate calculus expressing the %2total
correctness%1 of a program.  It is a kind of dual to the method
of inductive assertions invented by Robert Floyd which gives only
partial correctness, i.e. that the program give correct results
under the assumption that it terminates.  Manna's new method is
a creative achievement and elegantly presented, but  the Manna
sentences have been difficult to prove.  The method is ripe for
re-examination now that the techniques for proving such sentences
are better developed.

3. - with S. Ness and J. Vuillemin, "Inductive methods for proving
properties of programs", %2Communications of the ACM%1, vol. 16,
No. 8, ppl 491-502. (1973).

	This paper, which won an ACM award as the best paper of 1974,
presents several methods for proving properties of both recursive
and sequential programs.  One of the methods has been revived by
Morris and Wegbreit under the name of %2subgoal induction%1.
This method is for recursive programs what Floyd's inductive assertion
method is for sequential programs.

4. - with R. Waldinger, "Is "sometimes" sometimes better than always?
Intermittent assertions in proving program correctness", %2Communications
of the ACM%1, vol. 21, No. 2, pp. 159-172.  (February 1978).

	The paper suggests a new technique for program verification
which allows simpler and more intuitive proofs of many program
properties including termination.

	The paper has had a substantial impact on program verification
research since it was first presented at the Second International
Conference on Software Engineering (October 1976).  Many recent
papers discuss the technique, and several attempts have been made
to formalize the method.
.SKIP 2
!D  %3Current Research%*

Manna's current research is in three areas - mathematical theory of
computation, computer program synthesis, and other topics in theoretical
computer science.

	Manna has been one of the leaders in mathematical theory of
computation since his thesis in 1968.  He continues to develop new
techniques for proving that computer programs meet their specifications.
Thus, in collaboration with his student Nachum Dershowitz, he has
just completed a paper showing how production system computations
can be proved to terminate by induction on generalized lexicographic
orderings.  This has settled several previously recalcitrant cases.

	Within the last two years Manna has entered a new research
area - program synthesis.  He is trying to find relationships among
existing verification methods and to develop new ones.  Related efforts
are aimed at the automation of many of the processes a programmer
usually performs by hand such as debugging, documentation, modification
and optimization.  An ultimate goal of this research is the development
of synthesis techniques, by which the entire programming task is
performed automatically.

	If this work goes well, it will establish tighter connection
between Stanford work in theory of computation and the work in
artificial intelligence.
.next page
.once center
%3IV. THE CANDIDATE'S ROLE%*

A. Description of candidate's expected role.

	Manna will strengthen the Computer Science Department in mathematical
theory of computation and program synthesis.
When he was at
Stanford before he directed theses in mathematical theory of computation,
and his careful work with students has been missed.
He will teach the main courses and take part in curriculum design in these
areas.

	We also expect him to do his share of committee work, and we
consider him capable of taking his turn as department chairman.

B. He has already done all these things extremely successfully.

C. The department as a whole has connections with other departments, but
Manna's field is not especially involved in such collaborations.

D. When Manna was an assistant professor here at Stanford he took part
in the colloquium, library and curriculum committees.

At the Weizmann Institute, he was Head of the mathematics program and
a council member of the Feinberg Graduate School.  He has just been asked
to be chairman of the Department of Applied Mathematics and Dean of
the School of Mathematics.
.next page
.once center
%3V. EVALUATION OF TEACHING%*

!D  %3Ph.D. Students:%*
.skip
.begin nofill; PREFACE 0;
Jean-Marie Cadion (1972)
[Recursive Definitions of Partial Functions and their Computations]

Ashok Chandra (1973)
[On the Properties and Applications of Program Schemas]

Jean Vuillemin (1973)
[Proof Techniques for Recursive Programs]

Shmuel Katz (1976)
[Invariants and the Logical Analysis of Programs]

Adi Shamir (1977)
[Fixedpoints of Recursive Programs]

Nachum Dershowitz (1978)
[Automatic Program Modification]
.end

.PREFACE 1
!D %3Evaluation%*

	Manna is an excellent lecturer and is always extremely well
prepared.  Enclosed is a copy of the student course evaluation of his most
recent course taught at Stanford.  It is a research oriented course
in a field in which many of the students were unprepared.
His previous courses were taught before the Department established
formal course evaluation, but his reputation at that time was
excellent.
.next page
.once center
%3VI. SEARCH REPORT%*

	The Computer Science Department has been trying to get an
outstanding researcher and teacher in this field for many years.
In our letters concerning Manna we asked for comparison with the
outstanding people in the world, including Anthony Hoare and Dana Scott of
Oxford, Edsger Dijkstra, and Rod Burstall of Edinburgh.

	Scott was previously at Stanford in the Mathematics Department
and left for Princeton and finally Oxford.  His field overlaps Manna's
slightly, but his strengths are different.
He concentrates more on logic and philosophy and his computer work
is further from application.
We don't know why he left Stanford, but there is no reason to suppose
he wants to return.
Whether the Department would prefer him if were available has not been
explored.

	Hoare visited Stanford in 1973-74 and his interest in coming
to Stanford was explored with negative result; instead he moved from
Belfast to Oxford.  Whether we would now
prefer him is unexplored.

	Dijkstra declined a Stanford offer about five years ago.  The
Department would definitely not make him an offer today, because of
a conviction that he is not keeping up with what others have accomplished
in this field.

	Burstall's interest in coming to Stanford was explored several
years ago with negative results.  Whether we would prefer him, were
he available, has not been fully explored, but the general opinion is
that we would prefer Manna.

	If either Scott or Hoare were available, we would probably
consider them targets of opportunity.

	In our letters, we asked for recommendations of competitive
candidates and received none.

	We are confident that we know everyone who has made major
contributions to mathematical theory of computation.

	None of the outstanding people in this field are candidates
for affirmative action.
.skip 2
We are considering the appointment of Manna as a new appointment although
he has been here before.  However, because he has been here before,  the
senior faculty know Manna's work very well and unanimously support the
appointment.
∂24-Apr-78  1202	Levin at SUMEX-AIM 	brief biographical info on referees for manna
Date: 24 Apr 1978 1202-PST
From: Levin at SUMEX-AIM
Subject: brief biographical info on referees for manna
To:   jmc at SAIL
cc:   levin

john:
list of referees:
ashcroft
hansen
burstall
goldberg
hoare
igarashi
nilsson
nivat
pnueli
salomaa
waldinger
yeh
wegbreit
dijkstra

the note from the assoc. dean, Jim Rosse, said the report should
include..."a brief comment on the stature and competence to judge
the candidate of all referees whose judgments have a significant
bearing on the recommendation."
ed said this info should get to the dean soon, otherwise the process
will be delayed...let me know if there is anything that i can do...laurie
-------

	Edward Ashcroft is in the Computer Science Department at the 
University of Waterloo in Canada and knows about Manna's work on
proving parallel programs correct, because he collaborated with Manna
and has since pursued the subject separately.

	Per Brinch-Hansen is Chairman of the Computer Science Department
at U.S.C. and has worked on parallel processing and designing structured
operating systems.  While his letter is non-commital, he more recently
proposed Manna for the Jones Professorship at U.S.C.

	Anthony C. Hoare is Professor of Computer Science at Oxford
University and the discoverer of the Hoare formalism, one of the two
or three most popular lines of research in program proving.

	Shigeru Igarashi is Professor and Chairman at Tskuba University.
He has worked in program correctness since his thesis in 1964.

	Nils Nilsson is Staff Scientist at SRI.
He is the author of the leading older text on artificial intelligence.

	Rod Burstall is Reader in Computer Science at the University of
Edinburgh and one of the leading researchers in artificial intelligence
and mathematical theory of computation.

	Jack Goldberg is the head of Computer Science Research at SRI.

	Maurice Nivat is the leading French theorist in program correctness
and is Professor at the University of Paris.

	Amir Pnueli is another leading scientist in program proving
and is at the Weizmann Instititute.

	Arto Salomaa is Professor of Mathematics at the University of Turku
in Finland.  His work has mainly been in abstract automata theory
which overlaps Manna's intersts slightly.

	Richard Waldinger is a senior scientist at SRI and has collaborated
with Manna in writing a new book and in research on program synthesis.

	Raymond Yeh is Chairman of the Computer Science Department at
the University of Texas.

	Ben Wegbreit is at Xerox Palo Alto Research Center and formerly
at Harvard.  He also works in program proving and has further developed
a method originated by Manna and which he calls subgoal induction.

	Edsger Dijkstra is at one of the Dutch universities and is
Burroughs research fellow in computer science.  He is the author
of several texts and the originator of the doctrine of "structured
programming".

	Of these referees, the most prominent are Burstall, Dijkstra
and Hoare, who, not entirely co-incidentally, the only people who
were rated as comparable with Manna.
Some of the more non-commital were suggested by Manna, because he
thought he should suggest a number of department chairmen even if
they weren't active in his field.